↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
IN_ORDER_IN(tree(X, Left, Right), Xs) → U11(X, Left, Right, Xs, in_order_in(Left, Ls))
IN_ORDER_IN(tree(X, Left, Right), Xs) → IN_ORDER_IN(Left, Ls)
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → U21(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → IN_ORDER_IN(Right, Rs)
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U31(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → APP_IN(Ls, .(X, Rs), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U41(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
IN_ORDER_IN(tree(X, Left, Right), Xs) → U11(X, Left, Right, Xs, in_order_in(Left, Ls))
IN_ORDER_IN(tree(X, Left, Right), Xs) → IN_ORDER_IN(Left, Ls)
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → U21(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → IN_ORDER_IN(Right, Rs)
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U31(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → APP_IN(Ls, .(X, Rs), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U41(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PrologToPiTRSProof
APP_IN(.(Xs), Ys) → APP_IN(Xs, Ys)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
IN_ORDER_IN(tree(X, Left, Right), Xs) → IN_ORDER_IN(Left, Ls)
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → IN_ORDER_IN(Right, Rs)
IN_ORDER_IN(tree(X, Left, Right), Xs) → U11(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
IN_ORDER_IN → U11(in_order_in)
U11(in_order_out(Left, Ls)) → IN_ORDER_IN
IN_ORDER_IN → IN_ORDER_IN
in_order_in → U1(in_order_in)
in_order_in → in_order_out(void, [])
U1(in_order_out(Left, Ls)) → U2(Left, Ls, in_order_in)
U2(Left, Ls, in_order_out(Right, Rs)) → U3(Left, Right, app_in(Ls, .(Rs)))
app_in(.(Xs), Ys) → U4(app_in(Xs, Ys))
app_in([], X) → app_out(X)
U4(app_out(Zs)) → app_out(.(Zs))
U3(Left, Right, app_out(Xs)) → in_order_out(tree(Left, Right), Xs)
in_order_in
U1(x0)
U2(x0, x1, x2)
app_in(x0, x1)
U4(x0)
U3(x0, x1, x2)
IN_ORDER_IN → U11(in_order_out(void, []))
IN_ORDER_IN → U11(U1(in_order_in))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
IN_ORDER_IN → U11(in_order_out(void, []))
IN_ORDER_IN → U11(U1(in_order_in))
U11(in_order_out(Left, Ls)) → IN_ORDER_IN
IN_ORDER_IN → IN_ORDER_IN
in_order_in → U1(in_order_in)
in_order_in → in_order_out(void, [])
U1(in_order_out(Left, Ls)) → U2(Left, Ls, in_order_in)
U2(Left, Ls, in_order_out(Right, Rs)) → U3(Left, Right, app_in(Ls, .(Rs)))
app_in(.(Xs), Ys) → U4(app_in(Xs, Ys))
app_in([], X) → app_out(X)
U4(app_out(Zs)) → app_out(.(Zs))
U3(Left, Right, app_out(Xs)) → in_order_out(tree(Left, Right), Xs)
in_order_in
U1(x0)
U2(x0, x1, x2)
app_in(x0, x1)
U4(x0)
U3(x0, x1, x2)
IN_ORDER_IN → U11(in_order_out(void, []))
IN_ORDER_IN → U11(U1(in_order_in))
U11(in_order_out(Left, Ls)) → IN_ORDER_IN
IN_ORDER_IN → IN_ORDER_IN
in_order_in → U1(in_order_in)
in_order_in → in_order_out(void, [])
U1(in_order_out(Left, Ls)) → U2(Left, Ls, in_order_in)
U2(Left, Ls, in_order_out(Right, Rs)) → U3(Left, Right, app_in(Ls, .(Rs)))
app_in(.(Xs), Ys) → U4(app_in(Xs, Ys))
app_in([], X) → app_out(X)
U4(app_out(Zs)) → app_out(.(Zs))
U3(Left, Right, app_out(Xs)) → in_order_out(tree(Left, Right), Xs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
IN_ORDER_IN(tree(X, Left, Right), Xs) → U11(X, Left, Right, Xs, in_order_in(Left, Ls))
IN_ORDER_IN(tree(X, Left, Right), Xs) → IN_ORDER_IN(Left, Ls)
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → U21(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → IN_ORDER_IN(Right, Rs)
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U31(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → APP_IN(Ls, .(X, Rs), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U41(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
IN_ORDER_IN(tree(X, Left, Right), Xs) → U11(X, Left, Right, Xs, in_order_in(Left, Ls))
IN_ORDER_IN(tree(X, Left, Right), Xs) → IN_ORDER_IN(Left, Ls)
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → U21(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → IN_ORDER_IN(Right, Rs)
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U31(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
U21(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → APP_IN(Ls, .(X, Rs), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U41(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
APP_IN(.(Xs), Ys) → APP_IN(Xs, Ys)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDPToQDPProof
IN_ORDER_IN(tree(X, Left, Right), Xs) → IN_ORDER_IN(Left, Ls)
U11(X, Left, Right, Xs, in_order_out(Left, Ls)) → IN_ORDER_IN(Right, Rs)
IN_ORDER_IN(tree(X, Left, Right), Xs) → U11(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(tree(X, Left, Right), Xs) → U1(X, Left, Right, Xs, in_order_in(Left, Ls))
in_order_in(void, []) → in_order_out(void, [])
U1(X, Left, Right, Xs, in_order_out(Left, Ls)) → U2(X, Left, Right, Xs, Ls, in_order_in(Right, Rs))
U2(X, Left, Right, Xs, Ls, in_order_out(Right, Rs)) → U3(X, Left, Right, Xs, app_in(Ls, .(X, Rs), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U4(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U4(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(X, Left, Right, Xs, app_out(Ls, .(X, Rs), Xs)) → in_order_out(tree(X, Left, Right), Xs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
IN_ORDER_IN → U11(in_order_in)
U11(in_order_out(Left, Ls)) → IN_ORDER_IN
IN_ORDER_IN → IN_ORDER_IN
in_order_in → U1(in_order_in)
in_order_in → in_order_out(void, [])
U1(in_order_out(Left, Ls)) → U2(Left, Ls, in_order_in)
U2(Left, Ls, in_order_out(Right, Rs)) → U3(Left, Right, app_in(Ls, .(Rs)))
app_in(.(Xs), Ys) → U4(Xs, Ys, app_in(Xs, Ys))
app_in([], X) → app_out([], X, X)
U4(Xs, Ys, app_out(Xs, Ys, Zs)) → app_out(.(Xs), Ys, .(Zs))
U3(Left, Right, app_out(Ls, .(Rs), Xs)) → in_order_out(tree(Left, Right), Xs)
in_order_in
U1(x0)
U2(x0, x1, x2)
app_in(x0, x1)
U4(x0, x1, x2)
U3(x0, x1, x2)
IN_ORDER_IN → U11(in_order_out(void, []))
IN_ORDER_IN → U11(U1(in_order_in))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ NonTerminationProof
IN_ORDER_IN → U11(in_order_out(void, []))
IN_ORDER_IN → U11(U1(in_order_in))
U11(in_order_out(Left, Ls)) → IN_ORDER_IN
IN_ORDER_IN → IN_ORDER_IN
in_order_in → U1(in_order_in)
in_order_in → in_order_out(void, [])
U1(in_order_out(Left, Ls)) → U2(Left, Ls, in_order_in)
U2(Left, Ls, in_order_out(Right, Rs)) → U3(Left, Right, app_in(Ls, .(Rs)))
app_in(.(Xs), Ys) → U4(Xs, Ys, app_in(Xs, Ys))
app_in([], X) → app_out([], X, X)
U4(Xs, Ys, app_out(Xs, Ys, Zs)) → app_out(.(Xs), Ys, .(Zs))
U3(Left, Right, app_out(Ls, .(Rs), Xs)) → in_order_out(tree(Left, Right), Xs)
in_order_in
U1(x0)
U2(x0, x1, x2)
app_in(x0, x1)
U4(x0, x1, x2)
U3(x0, x1, x2)
IN_ORDER_IN → U11(in_order_out(void, []))
IN_ORDER_IN → U11(U1(in_order_in))
U11(in_order_out(Left, Ls)) → IN_ORDER_IN
IN_ORDER_IN → IN_ORDER_IN
in_order_in → U1(in_order_in)
in_order_in → in_order_out(void, [])
U1(in_order_out(Left, Ls)) → U2(Left, Ls, in_order_in)
U2(Left, Ls, in_order_out(Right, Rs)) → U3(Left, Right, app_in(Ls, .(Rs)))
app_in(.(Xs), Ys) → U4(Xs, Ys, app_in(Xs, Ys))
app_in([], X) → app_out([], X, X)
U4(Xs, Ys, app_out(Xs, Ys, Zs)) → app_out(.(Xs), Ys, .(Zs))
U3(Left, Right, app_out(Ls, .(Rs), Xs)) → in_order_out(tree(Left, Right), Xs)